7.4 KB · ⇊ 5 parts · ⤓ Micron 7.4 KB · ⤓ HTML 22.2 KB

top

In computer science, a computation is said to diverge if it does not terminate or terminates in an exceptional state.cite-ref-1[1] Otherwise it is said to converge. In domains where computations are expected to be infinite, such as process calculi, a computation is said to diverge if it fails to be productive (i.e. to continue producing an action within a finite amount of time).

• Definitions

• Rewriting

• Denotational semantics

• Concurrency theory

• See also

• Notes

• References

Various subfields of computer science use varying, but mathematically precise, definitions of what it means for a computation to converge or diverge.

In abstract rewriting, an abstract rewriting system is called convergent if it is both confluent and terminating.cite-ref-footnotebaadernipkow19989-2-0[2]

The notation t ↓ n means that t reduces to normal form n in zero or more reductions, t↓ means t reduces to some normal form in zero or more reductions, and t↑ means t does not reduce to a normal form; the latter is impossible in a terminating rewriting system.

In the lambda calculus an expression is divergent if it has no normal form.cite-ref-footnotepierce200265-3-0[3]

In denotational semantics an object function f : A → B can be modelled as a mathematical function f : A ∪ ∪ { ⊥ ⊥ } → → B ∪ ∪ { ⊥ ⊥ } {\displaystyle f:A\cup \{\perp \}\rightarrow B\cup \{\perp \}} where ⊥ (bottom) indicates that the object function or its argument diverges.

In the calculus of communicating sequential processes (CSP), divergence occurs when a process performs an endless series of hidden actions.cite-ref-ucs-4-0[4] For example, consider the following process, defined by CSP notation: C l o c k = t i c k → → C l o c k {\displaystyle Clock=tick\rightarrow Clock} The traces of this process are defined as: traces ⁡ ⁡ ( C l o c k ) = { ⟨ ⟨ ⟩ ⟩ , ⟨ ⟨ t i c k ⟩ ⟩ , ⟨ ⟨ t i c k , t i c k ⟩ ⟩ , … … } = { t i c k } ∗ ∗ {\displaystyle \operatorname {traces} (Clock)=\{\langle \rangle ,\langle tick\rangle ,\langle tick,tick\rangle ,\ldots \}=\{tick\}^{*}} Now, consider the following process, which hides the tick event of the Clock process: P = C l o c k ∖ ∖ t i c k {\displaystyle P=Clock\setminus tick} As P {\displaystyle P} cannot do anything other than perform hidden actions forever, it is equivalent to the process that does nothing but diverge, denoted d i v {\displaystyle \mathbf {div} } . One semantic model of CSP is the failures-divergences model, which refines the stable failures model by distinguishing processes based on the sets of traces after which they can diverge.

• Infinite loop

• Termination analysis

cite-note-11. ↑ citerefc-a-r-hoare1969C.A.R. Hoare (Oct 1969). "An Axiomatic Basis for Computer Programming" (PDF). Communications of the ACM. 12 (10): 576–583. doi:10.1145/363235.363259. S2CID 207726175.

cite-note-footnotebaadernipkow19989-22. ↑ Baader & Nipkow 1998, p. 9.

cite-note-footnotepierce200265-33. ↑ Pierce 2002, p. 65.

cite-note-ucs-44. ↑ citerefroscoe2010Roscoe, A.W. (2010). Understanding Concurrent Systems. Texts in Computer Science. doi:10.1007/978-1-84882-258-0. ISBN 978-1-84882-257-3.

• citerefbaadernipkow1998Baader, Franz; Nipkow, Tobias (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.

• citerefpierce2002Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press.

• J. M. R. Martin and S. A. Jassim (1997). "How to Design Deadlock-Free Networks Using CSP and Verification Tools: A Tutorial Introduction" in Proceedings of the WoTUG-20.